es:ES, e2, e1:E. e1  e2   (last([e1, e2]) ~ e2) 

latex

Definitions	ES, t  T, x:A. B(x), E, e  e' , P  Q, Top, before(e), es-ble{i:l}(es;e;e'), [e, e'], False, A, b, Prop, {T}, SQType(T), last(L), P & Q, P  Q, b, , Unit, filter(P;l), loc(e), Id, S  T, hd(l), i<j, ij, l[i]
Lemmas	last append, es-before wf2, Id wf, es-loc wf, filter wf, subtype rel list, top wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, not functionality wrt iff, assert-es-ble, false wf, assert wf, filter append sq, es-ble wf, es-before wf, es-le wf, es-E wf, event system wf